\begin{tabbing}
fischer{-}delay\=\{\=i:l,\+\+
\\[0ex]\$x:ut2,
\\[0ex]\$try:ut2,
\\[0ex]\$taken:ut2,
\\[0ex]\$contending:ut2,
\\[0ex]\$free:ut2,
\\[0ex]\$mine:ut2,
\\[0ex]\$wanted:ut2,
\\[0ex]\$z:ut2\}
\-\\[0ex](${\it es}$; ${\it del}$; $L$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$e$:es{-}E(${\it es}$). \+
\\[0ex](loc($e$) $\in$ $L$)
\\[0ex]$\Rightarrow$ \=(\=((@$e$(mkid\{\$x:ut2\}$\rightarrow$mkid\{\$try:ut2\}) $\vee$ @$e$(mkid\{\$x:ut2\}$\rightarrow$mkid\{\$taken:ut2\}))\+\+
\\[0ex]$\Rightarrow$ \=(((es{-}when(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$free:ut2\})\+
\\[0ex]$\Rightarrow$ (mkid\{\$x:ut2\} unchanged{-}for ${\it del}$ @ $e$))
\\[0ex]$\wedge$ \=((es{-}when(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$contending:ut2\})\+
\\[0ex]$\Rightarrow$ (mkid\{\$x:ut2\} unchanged{-}for 2 $\ast$ ${\it del}$ @ $e$))))
\-\-\-\\[0ex]$\wedge$ (@$e$(mkid\{\$x:ut2\}$\rightarrow$mkid\{\$mine:ut2\}) $\Rightarrow$ (mkid\{\$x:ut2\} unchanged{-}for 2 $\ast$ ${\it del}$ @ $e$))
\\[0ex]$\wedge$ \=(((((es{-}when(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$contending:ut2\})\+
\\[0ex]$\wedge$ (mkid\{\$x:ut2\} unchanged{-}for 2 $\ast$ ${\it del}$ @ $e$))
\\[0ex]$\vee$ \=((es{-}when(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$free:ut2\})\+
\\[0ex]$\wedge$ (mkid\{\$x:ut2\} unchanged{-}for ${\it del}$ @ $e$)))
\-\\[0ex]$\wedge$ \=(($\uparrow$es{-}isrcv(${\it es}$; $e$))\+
\\[0ex]c$\wedge$ \=((es{-}tag(${\it es}$; $e$) = mkid\{\$wanted:ut2\})\+
\\[0ex]$\wedge$ ($\exists$$i$:Id. (($i$ $\in$ $L$) $\wedge$ (es{-}lnk(${\it es}$; $e$) = $<$$i$, loc($e$), mkid\{\$z:ut2\}$>$))))))
\-\-\\[0ex]$\Rightarrow$ @$e$(mkid\{\$x:ut2\}$\rightarrow$mkid\{\$taken:ut2\}))
\-\\[0ex]$\wedge$ \=(($\uparrow$es{-}isrcv(${\it es}$; $e$))\+
\\[0ex]$\Rightarrow$ ((es{-}tag(${\it es}$; $e$) = mkid\{\$free:ut2\}) $\vee$ (es{-}tag(${\it es}$; $e$) = mkid\{\$wanted:ut2\}))
\\[0ex]$\Rightarrow$ ($\exists$\=$i$:Id\+
\\[0ex](($i$ $\in$ $L$) $\wedge$ ($\neg$($i$ = loc($e$))) $\wedge$ (es{-}lnk(${\it es}$; $e$) = $<$$i$, loc($e$), mkid\{\$z:ut2\}$>$)))
\-\\[0ex]$\Rightarrow$ qless(es{-}time(${\it es}$; $e$); (es{-}time(${\it es}$; es{-}sender(${\it es}$; $e$)) + ${\it del}$))))
\-\-\-
\end{tabbing}